COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	%elepha[w87,jmc]		Improvements to Elephant
C00005 00003	\section{References:}
C00006 00004	\centerline{This draft of \jobname\ TEXed on \jmcdate\ at \theTime}
C00008 ENDMK
C⊗;
%elepha[w87,jmc]		Improvements to Elephant
\input memo.tex[let,jmc]
\title{Improving Elephant by Increased Reification}

	We can make the correspondence between Elephant and Algolic
programming languages closer while maintaining the property
of Elephant that all properties of the program are logical
consequences of the sentence defining the program.  The idea
is to reify states and to use the functions $c(var,state)$
and $a(var,value,state)$ introduced in (McCarthy 1963).
These functions give the {\it contents} of a {\it variable}
in a {\it state} and the new state that results from assigning
a {\it value} to the variable in the old state.  They are
axiomatized in that paper.  We further use expression constants
and suppose that a function giving the value of an expression
in a state has been defined using the abstract syntax introduced
in (McCarthy 1963).

	We introduce the idea by writing the same old program
for doing multiplication by addition.  It is
%
$$\xi(t+1) = (λ pc)(\qif pc = start \qthen assign("i", n,\xi(t))
\qelseif pc = start+1 \qthen assign("p",0,\xi(t))
\qelseif pc = loop \qthen (\qif c("i",\xi(t)) = 0 \qthen goto(done,\xi(t))
\qelse n(\xi(t)))
\qelseif pc = loop+1 \qthen assign("p","p+m",\xi(t))
\qelseif pc = loop+2 \qthen assign("i","i-1",\xi(t))
\qelseif pc = loop+3 \qthen goto(loop,\xi(t))
\qelse \xi(t+1)) (c("pc",\xi(t))).$$
%
\section{References:}
{\bf McCarthy, John (1963)}: ``Towards a Mathematical Theory of Computation'',
in Proc.  IFIP Congress 62, North-Holland, Amsterdam.
\centerline{This draft of \jobname\ TEXed on \jmcdate\ at \theTime}
\centerline{Copyright \copyright\ \number\year\ by John McCarthy}
\vfill\eject\end